Termination Proof Script

• Consider the SCC {16,17}. There are no usable rules. By taking the AF π with π(A__LENGTH) = π(A__LENGTH1) = 1 and π(cons) = [2] together with the lexicographic path order with empty precedence, rule 17 is weakly decreasing and rule 16 is strictly decreasing.


• Consider the SCC {15,18,19,22,23}. By taking the AF π with π(A__FROM) = π(cons) = π(mark) = π(MARK) = π(s) = 1 and π(a__length) = π(a__length1) = π(length) = π(length1) = [ ] together with the lexicographic path order with precedence a__length ≻ 0, a__from ≈ from and a__length ≈ length ≈ a__length1 ≈ length1, the rules in {3-15,22,23} are weakly decreasing and the rules in {1,2,18,19} are strictly decreasing. There is one new SCC.
  • Consider the SCC {22,23}. There are no usable rules. By taking the AF π with π(cons) = π(MARK) = 1 together with the lexicographic path order with empty precedence, rule 22 is weakly decreasing and rule 23 is strictly decreasing. There is one new SCC.
    • Consider the SCC {22}. By taking the AF π with π(MARK) = 1 and π(cons) = [1] together with the lexicographic path order with empty precedence, rule 22 is strictly decreasing.